Nuprl Lemma : upto_is_nil
0,22
postcript
pdf
n
:
. upto(
n
) = nil
List
n
= 0
latex
Definitions
||
as
||
,
P
Q
,
P
&
Q
,
P
Q
,
upto(
n
)
,
S
T
,
{
i
..
j
}
,
A
B
,
A
,
False
,
P
Q
,
Prop
,
x
:
A
.
B
(
x
)
,
t
T
,
Lemmas
nat
wf
,
int
seg
wf
,
upto
wf
,
length
wf1
,
length
upto
,
le
wf
origin
n:
. upto(n) = nil 
List 
n = 0 n:. upto(n) = nil List n = 0 Q
Q
T
}
B
A Qx:A. B(x) T